$\forall$${\it es}$:ES\{i\}, $C$, $R$:Type\{i\}, $F$:(($C$ List)$\rightarrow$$R$), $I$:AbsInterface($C$), $O$:AbsInterface($R$).
\\[0ex]state{-}machine{-}spec\{i:l\}(${\it es}$; $C$; $R$; $F$; $I$; $O$) $\in$ $\mathbb{P}$\{i'\}